***********************************************************

A horrible propositional problem from Pelletier, designed to bend ATPs.
Solved by the precursor program,

(<-kb [[[p <=> q] <=> r] <=> [p <=> [q <=> r]]])

run time: 0.078125 secs
142158 inferences, equality = false
depth = 20, complexity = 21, timeout = 60 secs
true

***********************************************************
Step 1

? (((p <=> q) <=> r) <=> (p <=> (q <=> r)))


> revsk
=============================
Step 2

? (((((((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))) & (((~ p) v ((~ q) v r)) v (r v (~ r)))) & (((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q)))))))) & ((((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))) & (((~ p) v ((~ r) v q)) v (r v (~ r)))) & (((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q))))))))) & (((((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))) & ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))))) & ((((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r))))) & (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r))))))) & ((((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))) & ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))) & ((((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q))))))))))) & ((((((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))) & ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))))) & (((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))))) & ((((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q))))) & ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q)))))) & ((((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r)))))))))) & (((((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v p)) & (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r)))))))) & ((((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v p)) & (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r)))))))))))


> &r
|=============================
|Step 3
|
|? ((((((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))) & (((~ p) v ((~ q) v r)) v (r v (~ r)))) & (((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q)))))))) & ((((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))) & (((~ p) v ((~ r) v q)) v (r v (~ r)))) & (((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q))))))))) & (((((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))) & ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))))) & ((((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r))))) & (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r))))))) & ((((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))) & ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))) & ((((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q)))))))))))
|
|
|> &r
||=============================
||Step 4
||
||? (((((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))) & (((~ p) v ((~ q) v r)) v (r v (~ r)))) & (((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q)))))))) & ((((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))) & (((~ p) v ((~ r) v q)) v (r v (~ r)))) & (((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q)))))))))
||
||
||> &r
|||=============================
|||Step 5
|||
|||? ((((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))) & (((~ p) v ((~ q) v r)) v (r v (~ r)))) & (((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q))))))))
|||
|||
|||> &r
||||=============================
||||Step 6
||||
||||? (((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))) & (((~ p) v ((~ q) v r)) v (r v (~ r))))
||||
||||
||||> &r
|||||=============================
|||||Step 7
|||||
|||||? ((((~ p) v ((~ q) v r)) v (r v ((~ p) v q))) & (((~ p) v ((~ q) v r)) v (r v ((~ q) v p))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 8
||||||
||||||? (((~ p) v ((~ q) v r)) v (r v ((~ p) v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 9
||||||
||||||? q
||||||
||||||1. p
||||||2. (~ r)
||||||3. q
||||||
||||||> hyp
|||||=============================
|||||Step 10
|||||
|||||? (((~ p) v ((~ q) v r)) v (r v ((~ q) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 11
|||||
|||||? p
|||||
|||||1. q
|||||2. (~ r)
|||||3. p
|||||
|||||> hyp
||||=============================
||||Step 12
||||
||||? (((~ p) v ((~ q) v r)) v (r v (~ r)))
||||
||||
||||> hypdisj
||||=============================
||||Step 13
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. q
||||3. p
||||
||||> hyp
|||=============================
|||Step 14
|||
|||? (((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q)))))))
|||
|||
|||> &r
||||=============================
||||Step 15
||||
||||? ((((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q)))))))
||||
||||
||||> &r
|||||=============================
|||||Step 16
|||||
|||||? (((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q))))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 17
||||||
||||||? ((((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q)))))
||||||
||||||
||||||> &r
|||||||=============================
|||||||Step 18
|||||||
|||||||? (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v p)))
|||||||
|||||||
|||||||> hypdisj
|||||||=============================
|||||||Step 19
|||||||
|||||||? p
|||||||
|||||||1. (~ q)
|||||||2. p
|||||||3. (~ r)
|||||||4. q
|||||||
|||||||> hyp
||||||=============================
||||||Step 20
||||||
||||||? (((~ p) v ((~ q) v r)) v (((~ p) v q) v (q v (~ q))))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 21
||||||
||||||? (~ q)
||||||
||||||1. (~ q)
||||||2. p
||||||3. (~ r)
||||||
||||||> hyp
|||||=============================
|||||Step 22
|||||
|||||? ((((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 23
||||||
||||||? (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 24
||||||
||||||? p
||||||
||||||1. p
||||||2. (~ q)
||||||3. (~ r)
||||||4. q
||||||
||||||> hyp
|||||=============================
|||||Step 25
|||||
|||||? (((~ p) v ((~ q) v r)) v (((~ p) v q) v ((~ p) v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 26
|||||
|||||? (~ q)
|||||
|||||1. p
|||||2. (~ q)
|||||3. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 27
||||
||||? (((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 28
|||||
|||||? ((((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 29
||||||
||||||? (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 30
||||||
||||||? p
||||||
||||||1. (~ q)
||||||2. q
||||||3. (~ r)
||||||4. p
||||||
||||||> hyp
|||||=============================
|||||Step 31
|||||
|||||? (((~ p) v ((~ q) v r)) v (((~ q) v p) v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 32
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. (~ p)
|||||3. (~ r)
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 33
||||
||||? ((((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 34
|||||
|||||? (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 35
|||||
|||||? p
|||||
|||||1. p
|||||2. q
|||||3. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 36
||||
||||? (((~ p) v ((~ q) v r)) v (((~ q) v p) v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 37
||||
||||? (~ p)
||||
||||1. q
||||2. (~ p)
||||3. (~ r)
||||
||||> hyp
|||=============================
|||Step 38
|||
|||? (((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 39
||||
||||? ((((~ p) v ((~ q) v r)) v ((~ r) v (q v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 40
|||||
|||||? (((~ p) v ((~ q) v r)) v ((~ r) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 41
|||||
|||||? p
|||||
|||||1. (~ q)
|||||2. r
|||||3. (~ r)
|||||4. q
|||||5. p
|||||
|||||> hyp
||||=============================
||||Step 42
||||
||||? (((~ p) v ((~ q) v r)) v ((~ r) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 43
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. r
||||3. (~ r)
||||4. p
||||
||||> hyp
|||=============================
|||Step 44
|||
|||? ((((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 45
||||
||||? (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 46
||||
||||? p
||||
||||1. p
||||2. r
||||3. (~ r)
||||4. q
||||
||||> hyp
|||=============================
|||Step 47
|||
|||? (((~ p) v ((~ q) v r)) v ((~ r) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 48
|||
|||? (~ r)
|||
|||1. q
|||2. p
|||3. (~ r)
|||
|||> hyp
||=============================
||Step 49
||
||? ((((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))) & (((~ p) v ((~ r) v q)) v (r v (~ r)))) & (((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q))))))))
||
||
||> &r
|||=============================
|||Step 50
|||
|||? (((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))) & (((~ p) v ((~ r) v q)) v (r v (~ r))))
|||
|||
|||> &r
||||=============================
||||Step 51
||||
||||? ((((~ p) v ((~ r) v q)) v (r v ((~ p) v q))) & (((~ p) v ((~ r) v q)) v (r v ((~ q) v p))))
||||
||||
||||> &r
|||||=============================
|||||Step 52
|||||
|||||? (((~ p) v ((~ r) v q)) v (r v ((~ p) v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 53
|||||
|||||? r
|||||
|||||1. (~ q)
|||||2. p
|||||3. r
|||||
|||||> hyp
||||=============================
||||Step 54
||||
||||? (((~ p) v ((~ r) v q)) v (r v ((~ q) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 55
||||
||||? p
||||
||||1. q
||||2. (~ r)
||||3. (~ q)
||||4. r
||||5. p
||||
||||> hyp
|||=============================
|||Step 56
|||
|||? (((~ p) v ((~ r) v q)) v (r v (~ r)))
|||
|||
|||> hypdisj
|||=============================
|||Step 57
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. (~ q)
|||3. p
|||
|||> hyp
||=============================
||Step 58
||
||? (((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))) & (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q)))))))
||
||
||> &r
|||=============================
|||Step 59
|||
|||? ((((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))))
|||
|||
|||> &r
||||=============================
||||Step 60
||||
||||? (((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 61
|||||
|||||? ((((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 62
||||||
||||||? (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 63
||||||
||||||? p
||||||
||||||1. (~ q)
||||||2. p
||||||3. r
||||||
||||||> hyp
|||||=============================
|||||Step 64
|||||
|||||? (((~ p) v ((~ r) v q)) v (((~ p) v q) v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 65
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. p
|||||3. r
|||||
|||||> hyp
||||=============================
||||Step 66
||||
||||? ((((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 67
|||||
|||||? (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 68
|||||
|||||? p
|||||
|||||1. p
|||||2. (~ q)
|||||3. r
|||||
|||||> hyp
||||=============================
||||Step 69
||||
||||? (((~ p) v ((~ r) v q)) v (((~ p) v q) v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 70
||||
||||? (~ q)
||||
||||1. p
||||2. (~ q)
||||3. r
||||
||||> hyp
|||=============================
|||Step 71
|||
|||? (((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 72
||||
||||? ((((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 73
|||||
|||||? (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 74
|||||
|||||? p
|||||
|||||1. (~ q)
|||||2. q
|||||3. r
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 75
||||
||||? (((~ p) v ((~ r) v q)) v (((~ q) v p) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 76
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. (~ p)
||||3. r
||||4. p
||||
||||> hyp
|||=============================
|||Step 77
|||
|||? ((((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 78
||||
||||? (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 79
||||
||||? p
||||
||||1. p
||||2. q
||||3. (~ q)
||||4. r
||||
||||> hyp
|||=============================
|||Step 80
|||
|||? (((~ p) v ((~ r) v q)) v (((~ q) v p) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 81
|||
|||? (~ q)
|||
|||1. p
|||2. (~ p)
|||3. (~ q)
|||4. r
|||
|||> hyp
||=============================
||Step 82
||
||? (((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))) & ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q))))))
||
||
||> &r
|||=============================
|||Step 83
|||
|||? ((((~ p) v ((~ r) v q)) v ((~ r) v (q v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 84
||||
||||? (((~ p) v ((~ r) v q)) v ((~ r) v (q v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 85
||||
||||? p
||||
||||1. (~ q)
||||2. r
||||3. p
||||
||||> hyp
|||=============================
|||Step 86
|||
|||? (((~ p) v ((~ r) v q)) v ((~ r) v (q v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 87
|||
|||? (~ q)
|||
|||1. (~ q)
|||2. r
|||3. p
|||
|||> hyp
||=============================
||Step 88
||
||? ((((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p))) & (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q)))))
||
||
||> &r
|||=============================
|||Step 89
|||
|||? (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 90
|||
|||? p
|||
|||1. p
|||2. r
|||3. (~ q)
|||
|||> hyp
||=============================
||Step 91
||
||? (((~ p) v ((~ r) v q)) v ((~ r) v ((~ p) v (~ q))))
||
||
||> hypdisj
||=============================
||Step 92
||
||? (~ q)
||
||1. p
||2. r
||3. (~ q)
||
||> hyp
|=============================
|Step 93
|
|? (((((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))) & ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))))) & ((((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r))))) & (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r))))))) & ((((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))) & ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))) & ((((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q))))))))))
|
|
|> &r
||=============================
||Step 94
||
||? ((((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))) & ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))))) & ((((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r))))) & (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r)))))))
||
||
||> &r
|||=============================
|||Step 95
|||
|||? (((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))) & ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r)))))))
|||
|||
|||> &r
||||=============================
||||Step 96
||||
||||? ((((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r))))) & (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r))))))
||||
||||
||||> &r
|||||=============================
|||||Step 97
|||||
|||||? (((r v ((~ p) v q)) v (p v (r v q))) & ((r v ((~ p) v q)) v (p v (r v (~ r)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 98
||||||
||||||? ((r v ((~ p) v q)) v (p v (r v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 99
||||||
||||||? p
||||||
||||||1. (~ q)
||||||2. (~ r)
||||||3. p
||||||
||||||> hyp
|||||=============================
|||||Step 100
|||||
|||||? ((r v ((~ p) v q)) v (p v (r v (~ r))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 101
|||||
|||||? (~ r)
|||||
|||||1. (~ r)
|||||2. (~ p)
|||||3. (~ q)
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 102
||||
||||? (((r v ((~ q) v p)) v (p v (r v q))) & ((r v ((~ q) v p)) v (p v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 103
|||||
|||||? ((r v ((~ q) v p)) v (p v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 104
|||||
|||||? q
|||||
|||||1. (~ r)
|||||2. (~ p)
|||||3. q
|||||
|||||> hyp
||||=============================
||||Step 105
||||
||||? ((r v ((~ q) v p)) v (p v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 106
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. (~ p)
||||3. q
||||
||||> hyp
|||=============================
|||Step 107
|||
|||? ((((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))) & (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 108
||||
||||? (((r v ((~ p) v q)) v (p v ((~ q) v q))) & ((r v ((~ p) v q)) v (p v ((~ q) v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 109
|||||
|||||? ((r v ((~ p) v q)) v (p v ((~ q) v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 110
|||||
|||||? q
|||||
|||||1. q
|||||2. (~ p)
|||||3. p
|||||4. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 111
||||
||||? ((r v ((~ p) v q)) v (p v ((~ q) v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 112
||||
||||? (~ r)
||||
||||1. q
||||2. (~ p)
||||3. (~ q)
||||4. p
||||5. (~ r)
||||
||||> hyp
|||=============================
|||Step 113
|||
|||? (((r v ((~ q) v p)) v (p v ((~ q) v q))) & ((r v ((~ q) v p)) v (p v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 114
||||
||||? ((r v ((~ q) v p)) v (p v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 115
||||
||||? q
||||
||||1. q
||||2. (~ p)
||||3. (~ r)
||||
||||> hyp
|||=============================
|||Step 116
|||
|||? ((r v ((~ q) v p)) v (p v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 117
|||
|||? (~ r)
|||
|||1. q
|||2. (~ p)
|||3. (~ r)
|||
|||> hyp
||=============================
||Step 118
||
||? ((((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r))))) & (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 119
|||
|||? (((r v (~ r)) v (p v (r v q))) & ((r v (~ r)) v (p v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 120
||||
||||? ((r v (~ r)) v (p v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 121
||||
||||? r
||||
||||1. (~ q)
||||2. (~ p)
||||3. r
||||
||||> hyp
|||=============================
|||Step 122
|||
|||? ((r v (~ r)) v (p v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 123
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. (~ p)
|||
|||> hyp
||=============================
||Step 124
||
||? (((r v (~ r)) v (p v ((~ q) v q))) & ((r v (~ r)) v (p v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 125
|||
|||? ((r v (~ r)) v (p v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 126
|||
|||? q
|||
|||1. q
|||2. (~ p)
|||3. r
|||4. (~ r)
|||
|||> hyp
||=============================
||Step 127
||
||? ((r v (~ r)) v (p v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 128
||
||? (~ r)
||
||1. q
||2. (~ p)
||3. (~ r)
||
||> hyp
|=============================
|Step 129
|
|? ((((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))) & ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))) & ((((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q)))))))))
|
|
|> &r
||=============================
||Step 130
||
||? (((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))) & ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))))
||
||
||> &r
|||=============================
|||Step 131
|||
|||? ((((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))
|||
|||
|||> &r
||||=============================
||||Step 132
||||
||||? (((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q)))))))
||||
||||
||||> &r
|||||=============================
|||||Step 133
|||||
|||||? ((((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q))))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 134
||||||
||||||? (((p v (r v q)) v (((~ p) v q) v (q v p))) & ((p v (r v q)) v (((~ p) v q) v (q v (~ q)))))
||||||
||||||
||||||> &r
|||||||=============================
|||||||Step 135
|||||||
|||||||? ((p v (r v q)) v (((~ p) v q) v (q v p)))
|||||||
|||||||
|||||||> hypdisj
|||||||=============================
|||||||Step 136
|||||||
|||||||? p
|||||||
|||||||1. (~ q)
|||||||2. p
|||||||3. (~ r)
|||||||
|||||||> hyp
||||||=============================
||||||Step 137
||||||
||||||? ((p v (r v q)) v (((~ p) v q) v (q v (~ q))))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 138
||||||
||||||? (~ q)
||||||
||||||1. (~ q)
||||||2. p
||||||3. (~ r)
||||||4. (~ p)
||||||
||||||> hyp
|||||=============================
|||||Step 139
|||||
|||||? (((p v (r v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 140
||||||
||||||? ((p v (r v q)) v (((~ p) v q) v ((~ p) v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 141
||||||
||||||? p
||||||
||||||1. p
||||||2. (~ q)
||||||3. (~ r)
||||||
||||||> hyp
|||||=============================
|||||Step 142
|||||
|||||? ((p v (r v q)) v (((~ p) v q) v ((~ p) v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 143
|||||
|||||? (~ q)
|||||
|||||1. p
|||||2. (~ q)
|||||3. (~ r)
|||||4. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 144
||||
||||? ((((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 145
|||||
|||||? (((p v (r v (~ r))) v (((~ p) v q) v (q v p))) & ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 146
||||||
||||||? ((p v (r v (~ r))) v (((~ p) v q) v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 147
||||||
||||||? p
||||||
||||||1. (~ q)
||||||2. p
||||||3. r
||||||4. (~ r)
||||||
||||||> hyp
|||||=============================
|||||Step 148
|||||
|||||? ((p v (r v (~ r))) v (((~ p) v q) v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 149
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. p
|||||3. r
|||||4. (~ r)
|||||5. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 150
||||
||||? (((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 151
|||||
|||||? ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 152
|||||
|||||? p
|||||
|||||1. p
|||||2. (~ q)
|||||3. r
|||||4. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 153
||||
||||? ((p v (r v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 154
||||
||||? (~ q)
||||
||||1. p
||||2. (~ q)
||||3. r
||||4. (~ r)
||||5. (~ p)
||||
||||> hyp
|||=============================
|||Step 155
|||
|||? (((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))
|||
|||
|||> &r
||||=============================
||||Step 156
||||
||||? ((((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 157
|||||
|||||? (((p v (r v q)) v (((~ q) v p) v (q v p))) & ((p v (r v q)) v (((~ q) v p) v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 158
||||||
||||||? ((p v (r v q)) v (((~ q) v p) v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 159
||||||
||||||? q
||||||
||||||1. (~ p)
||||||2. q
||||||3. (~ r)
||||||
||||||> hyp
|||||=============================
|||||Step 160
|||||
|||||? ((p v (r v q)) v (((~ q) v p) v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 161
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. (~ p)
|||||3. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 162
||||
||||? (((p v (r v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 163
|||||
|||||? ((p v (r v q)) v (((~ q) v p) v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 164
|||||
|||||? p
|||||
|||||1. p
|||||2. q
|||||3. (~ q)
|||||4. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 165
||||
||||? ((p v (r v q)) v (((~ q) v p) v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 166
||||
||||? (~ q)
||||
||||1. p
||||2. (~ p)
||||3. (~ q)
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 167
|||
|||? ((((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 168
||||
||||? (((p v (r v (~ r))) v (((~ q) v p) v (q v p))) & ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 169
|||||
|||||? ((p v (r v (~ r))) v (((~ q) v p) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 170
|||||
|||||? q
|||||
|||||1. (~ p)
|||||2. q
|||||3. r
|||||4. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 171
||||
||||? ((p v (r v (~ r))) v (((~ q) v p) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 172
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. (~ p)
||||3. r
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 173
|||
|||? (((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 174
||||
||||? ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 175
||||
||||? p
||||
||||1. p
||||2. q
||||3. r
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 176
|||
|||? ((p v (r v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 177
|||
|||? (~ p)
|||
|||1. q
|||2. (~ p)
|||3. r
|||4. (~ r)
|||
|||> hyp
||=============================
||Step 178
||
||? ((((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))))
||
||
||> &r
|||=============================
|||Step 179
|||
|||? (((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q)))))))
|||
|||
|||> &r
||||=============================
||||Step 180
||||
||||? ((((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 181
|||||
|||||? (((p v ((~ q) v q)) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 182
||||||
||||||? ((p v ((~ q) v q)) v (((~ p) v q) v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 183
||||||
||||||? p
||||||
||||||1. (~ q)
||||||2. p
||||||3. q
||||||
||||||> hyp
|||||=============================
|||||Step 184
|||||
|||||? ((p v ((~ q) v q)) v (((~ p) v q) v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 185
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. p
|||||3. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 186
||||
||||? (((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 187
|||||
|||||? ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 188
|||||
|||||? p
|||||
|||||1. p
|||||2. (~ q)
|||||3. q
|||||
|||||> hyp
||||=============================
||||Step 189
||||
||||? ((p v ((~ q) v q)) v (((~ p) v q) v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 190
||||
||||? (~ q)
||||
||||1. p
||||2. (~ q)
||||3. (~ p)
||||
||||> hyp
|||=============================
|||Step 191
|||
|||? ((((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 192
||||
||||? (((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 193
|||||
|||||? ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 194
|||||
|||||? p
|||||
|||||1. (~ q)
|||||2. p
|||||3. r
|||||4. q
|||||
|||||> hyp
||||=============================
||||Step 195
||||
||||? ((p v ((~ q) v (~ r))) v (((~ p) v q) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 196
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. p
||||3. r
||||4. (~ p)
||||
||||> hyp
|||=============================
|||Step 197
|||
|||? (((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 198
||||
||||? ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 199
||||
||||? p
||||
||||1. p
||||2. (~ q)
||||3. r
||||4. q
||||
||||> hyp
|||=============================
|||Step 200
|||
|||? ((p v ((~ q) v (~ r))) v (((~ p) v q) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 201
|||
|||? (~ q)
|||
|||1. p
|||2. (~ q)
|||3. r
|||4. (~ p)
|||
|||> hyp
||=============================
||Step 202
||
||? (((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))))
||
||
||> &r
|||=============================
|||Step 203
|||
|||? ((((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 204
||||
||||? (((p v ((~ q) v q)) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 205
|||||
|||||? ((p v ((~ q) v q)) v (((~ q) v p) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 206
|||||
|||||? q
|||||
|||||1. (~ p)
|||||2. q
|||||
|||||> hyp
||||=============================
||||Step 207
||||
||||? ((p v ((~ q) v q)) v (((~ q) v p) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 208
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. (~ p)
||||
||||> hyp
|||=============================
|||Step 209
|||
|||? (((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 210
||||
||||? ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 211
||||
||||? p
||||
||||1. p
||||2. q
||||3. (~ q)
||||
||||> hyp
|||=============================
|||Step 212
|||
|||? ((p v ((~ q) v q)) v (((~ q) v p) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 213
|||
|||? (~ q)
|||
|||1. p
|||2. (~ p)
|||3. (~ q)
|||
|||> hyp
||=============================
||Step 214
||
||? ((((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))))
||
||
||> &r
|||=============================
|||Step 215
|||
|||? (((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 216
||||
||||? ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 217
||||
||||? q
||||
||||1. (~ p)
||||2. q
||||3. r
||||
||||> hyp
|||=============================
|||Step 218
|||
|||? ((p v ((~ q) v (~ r))) v (((~ q) v p) v (q v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 219
|||
|||? (~ q)
|||
|||1. (~ q)
|||2. (~ p)
|||3. r
|||
|||> hyp
||=============================
||Step 220
||
||? (((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q)))))
||
||
||> &r
|||=============================
|||Step 221
|||
|||? ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 222
|||
|||? p
|||
|||1. p
|||2. q
|||3. r
|||
|||> hyp
||=============================
||Step 223
||
||? ((p v ((~ q) v (~ r))) v (((~ q) v p) v ((~ p) v (~ q))))
||
||
||> hypdisj
||=============================
||Step 224
||
||? (~ p)
||
||1. q
||2. (~ p)
||3. r
||
||> hyp
|=============================
|Step 225
|
|? ((((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))) & (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q))))))))
|
|
|> &r
||=============================
||Step 226
||
||? (((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q)))))))
||
||
||> &r
|||=============================
|||Step 227
|||
|||? ((((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q))))) & (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 228
||||
||||? (((p v (r v q)) v ((~ r) v (q v p))) & ((p v (r v q)) v ((~ r) v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 229
|||||
|||||? ((p v (r v q)) v ((~ r) v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 230
|||||
|||||? (~ r)
|||||
|||||1. (~ p)
|||||2. (~ q)
|||||3. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 231
||||
||||? ((p v (r v q)) v ((~ r) v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 232
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. r
||||3. (~ r)
||||4. (~ p)
||||
||||> hyp
|||=============================
|||Step 233
|||
|||? (((p v (r v q)) v ((~ r) v ((~ p) v p))) & ((p v (r v q)) v ((~ r) v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 234
||||
||||? ((p v (r v q)) v ((~ r) v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 235
||||
||||? p
||||
||||1. p
||||2. r
||||3. (~ q)
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 236
|||
|||? ((p v (r v q)) v ((~ r) v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 237
|||
|||? (~ q)
|||
|||1. p
|||2. r
|||3. (~ q)
|||4. (~ r)
|||5. (~ p)
|||
|||> hyp
||=============================
||Step 238
||
||? ((((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))))
||
||
||> &r
|||=============================
|||Step 239
|||
|||? (((p v (r v (~ r))) v ((~ r) v (q v p))) & ((p v (r v (~ r))) v ((~ r) v (q v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 240
||||
||||? ((p v (r v (~ r))) v ((~ r) v (q v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 241
||||
||||? (~ r)
||||
||||1. (~ p)
||||2. (~ q)
||||3. (~ r)
||||
||||> hyp
|||=============================
|||Step 242
|||
|||? ((p v (r v (~ r))) v ((~ r) v (q v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 243
|||
|||? (~ q)
|||
|||1. (~ q)
|||2. r
|||3. (~ r)
|||4. (~ p)
|||
|||> hyp
||=============================
||Step 244
||
||? (((p v (r v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q)))))
||
||
||> &r
|||=============================
|||Step 245
|||
|||? ((p v (r v (~ r))) v ((~ r) v ((~ p) v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 246
|||
|||? p
|||
|||1. p
|||2. r
|||3. (~ r)
|||
|||> hyp
||=============================
||Step 247
||
||? ((p v (r v (~ r))) v ((~ r) v ((~ p) v (~ q))))
||
||
||> hypdisj
||=============================
||Step 248
||
||? (~ p)
||
||1. q
||2. r
||3. (~ r)
||4. (~ p)
||
||> hyp
|=============================
|Step 249
|
|? (((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))) & ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q)))))))
|
|
|> &r
||=============================
||Step 250
||
||? ((((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q))))))
||
||
||> &r
|||=============================
|||Step 251
|||
|||? (((p v ((~ q) v q)) v ((~ r) v (q v p))) & ((p v ((~ q) v q)) v ((~ r) v (q v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 252
||||
||||? ((p v ((~ q) v q)) v ((~ r) v (q v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 253
||||
||||? q
||||
||||1. (~ p)
||||2. r
||||3. q
||||
||||> hyp
|||=============================
|||Step 254
|||
|||? ((p v ((~ q) v q)) v ((~ r) v (q v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 255
|||
|||? (~ q)
|||
|||1. (~ q)
|||2. r
|||3. (~ p)
|||
|||> hyp
||=============================
||Step 256
||
||? (((p v ((~ q) v q)) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q)))))
||
||
||> &r
|||=============================
|||Step 257
|||
|||? ((p v ((~ q) v q)) v ((~ r) v ((~ p) v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 258
|||
|||? p
|||
|||1. p
|||2. r
|||3. (~ q)
|||4. q
|||
|||> hyp
||=============================
||Step 259
||
||? ((p v ((~ q) v q)) v ((~ r) v ((~ p) v (~ q))))
||
||
||> hypdisj
||=============================
||Step 260
||
||? (~ q)
||
||1. p
||2. r
||3. (~ q)
||4. (~ p)
||
||> hyp
|=============================
|Step 261
|
|? ((((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))) & (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q))))))
|
|
|> &r
||=============================
||Step 262
||
||? (((p v ((~ q) v (~ r))) v ((~ r) v (q v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q)))))
||
||
||> &r
|||=============================
|||Step 263
|||
|||? ((p v ((~ q) v (~ r))) v ((~ r) v (q v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 264
|||
|||? q
|||
|||1. (~ p)
|||2. r
|||3. q
|||
|||> hyp
||=============================
||Step 265
||
||? ((p v ((~ q) v (~ r))) v ((~ r) v (q v (~ q))))
||
||
||> hypdisj
||=============================
||Step 266
||
||? (~ q)
||
||1. (~ q)
||2. r
||3. (~ p)
||
||> hyp
|=============================
|Step 267
|
|? (((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p))) & ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q)))))
|
|
|> &r
||=============================
||Step 268
||
||? ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v p)))
||
||
||> hypdisj
||=============================
||Step 269
||
||? p
||
||1. p
||2. r
||3. q
||
||> hyp
|=============================
|Step 270
|
|? ((p v ((~ q) v (~ r))) v ((~ r) v ((~ p) v (~ q))))
|
|
|> hypdisj
|=============================
|Step 271
|
|? (~ p)
|
|1. q
|2. r
|3. (~ p)
|
|> hyp
=============================
Step 272

? ((((((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))) & ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))))) & (((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))))) & ((((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q))))) & ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q)))))) & ((((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r)))))))))) & (((((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v p)) & (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r)))))))) & ((((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v p)) & (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r))))))))))


> &r
|=============================
|Step 273
|
|? (((((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))) & ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))))) & (((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))))) & ((((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q))))) & ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q)))))) & ((((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r))))))))))
|
|
|> &r
||=============================
||Step 274
||
||? ((((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))) & ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))))) & (((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))))))))
||
||
||> &r
|||=============================
|||Step 275
|||
|||? (((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))) & ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q)))))))
|||
|||
|||> &r
||||=============================
||||Step 276
||||
||||? ((((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q))))) & (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q))))))
||||
||||
||||> &r
|||||=============================
|||||Step 277
|||||
|||||? (((p v ((~ q) v r)) v (r v (q v p))) & ((p v ((~ q) v r)) v (r v (q v (~ q)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 278
||||||
||||||? ((p v ((~ q) v r)) v (r v (q v p)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 279
||||||
||||||? q
||||||
||||||1. (~ p)
||||||2. (~ r)
||||||3. q
||||||
||||||> hyp
|||||=============================
|||||Step 280
|||||
|||||? ((p v ((~ q) v r)) v (r v (q v (~ q))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 281
|||||
|||||? (~ q)
|||||
|||||1. (~ q)
|||||2. (~ r)
|||||3. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 282
||||
||||? (((p v ((~ r) v q)) v (r v (q v p))) & ((p v ((~ r) v q)) v (r v (q v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 283
|||||
|||||? ((p v ((~ r) v q)) v (r v (q v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 284
|||||
|||||? r
|||||
|||||1. (~ p)
|||||2. (~ q)
|||||3. r
|||||
|||||> hyp
||||=============================
||||Step 285
||||
||||? ((p v ((~ r) v q)) v (r v (q v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 286
||||
||||? (~ q)
||||
||||1. (~ q)
||||2. (~ r)
||||3. r
||||4. (~ p)
||||
||||> hyp
|||=============================
|||Step 287
|||
|||? ((((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))) & (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))))
|||
|||
|||> &r
||||=============================
||||Step 288
||||
||||? (((p v ((~ q) v r)) v (r v ((~ p) v p))) & ((p v ((~ q) v r)) v (r v ((~ p) v (~ q)))))
||||
||||
||||> &r
|||||=============================
|||||Step 289
|||||
|||||? ((p v ((~ q) v r)) v (r v ((~ p) v p)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 290
|||||
|||||? p
|||||
|||||1. p
|||||2. (~ r)
|||||3. q
|||||
|||||> hyp
||||=============================
||||Step 291
||||
||||? ((p v ((~ q) v r)) v (r v ((~ p) v (~ q))))
||||
||||
||||> hypdisj
||||=============================
||||Step 292
||||
||||? (~ p)
||||
||||1. q
||||2. (~ r)
||||3. (~ p)
||||
||||> hyp
|||=============================
|||Step 293
|||
|||? (((p v ((~ r) v q)) v (r v ((~ p) v p))) & ((p v ((~ r) v q)) v (r v ((~ p) v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 294
||||
||||? ((p v ((~ r) v q)) v (r v ((~ p) v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 295
||||
||||? p
||||
||||1. p
||||2. (~ r)
||||3. (~ q)
||||4. r
||||
||||> hyp
|||=============================
|||Step 296
|||
|||? ((p v ((~ r) v q)) v (r v ((~ p) v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 297
|||
|||? (~ q)
|||
|||1. p
|||2. (~ r)
|||3. (~ q)
|||4. r
|||5. (~ p)
|||
|||> hyp
||=============================
||Step 298
||
||? (((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))))
||
||
||> &r
|||=============================
|||Step 299
|||
|||? ((((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))))))
|||
|||
|||> &r
||||=============================
||||Step 300
||||
||||? (((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r)))))))
||||
||||
||||> &r
|||||=============================
|||||Step 301
|||||
|||||? ((((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r))))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 302
||||||
||||||? (((r v (q v p)) v (((~ q) v r) v (r v q))) & ((r v (q v p)) v (((~ q) v r) v (r v (~ r)))))
||||||
||||||
||||||> &r
|||||||=============================
|||||||Step 303
|||||||
|||||||? ((r v (q v p)) v (((~ q) v r) v (r v q)))
|||||||
|||||||
|||||||> hypdisj
|||||||=============================
|||||||Step 304
|||||||
|||||||? q
|||||||
|||||||1. (~ r)
|||||||2. q
|||||||3. (~ p)
|||||||
|||||||> hyp
||||||=============================
||||||Step 305
||||||
||||||? ((r v (q v p)) v (((~ q) v r) v (r v (~ r))))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 306
||||||
||||||? (~ r)
||||||
||||||1. (~ r)
||||||2. q
||||||3. (~ p)
||||||4. (~ q)
||||||
||||||> hyp
|||||=============================
|||||Step 307
|||||
|||||? (((r v (q v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 308
||||||
||||||? ((r v (q v p)) v (((~ q) v r) v ((~ q) v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 309
||||||
||||||? q
||||||
||||||1. q
||||||2. (~ r)
||||||3. (~ p)
||||||
||||||> hyp
|||||=============================
|||||Step 310
|||||
|||||? ((r v (q v p)) v (((~ q) v r) v ((~ q) v (~ r))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 311
|||||
|||||? (~ r)
|||||
|||||1. q
|||||2. (~ r)
|||||3. (~ p)
|||||4. (~ q)
|||||
|||||> hyp
||||=============================
||||Step 312
||||
||||? ((((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))
||||
||||
||||> &r
|||||=============================
|||||Step 313
|||||
|||||? (((r v (q v (~ q))) v (((~ q) v r) v (r v q))) & ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 314
||||||
||||||? ((r v (q v (~ q))) v (((~ q) v r) v (r v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 315
||||||
||||||? q
||||||
||||||1. (~ r)
||||||2. q
||||||
||||||> hyp
|||||=============================
|||||Step 316
|||||
|||||? ((r v (q v (~ q))) v (((~ q) v r) v (r v (~ r))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 317
|||||
|||||? (~ r)
|||||
|||||1. (~ r)
|||||2. q
|||||3. (~ q)
|||||
|||||> hyp
||||=============================
||||Step 318
||||
||||? (((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 319
|||||
|||||? ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 320
|||||
|||||? q
|||||
|||||1. q
|||||2. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 321
||||
||||? ((r v (q v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 322
||||
||||? (~ r)
||||
||||1. q
||||2. (~ r)
||||3. (~ q)
||||
||||> hyp
|||=============================
|||Step 323
|||
|||? (((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))
|||
|||
|||> &r
||||=============================
||||Step 324
||||
||||? ((((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r))))))
||||
||||
||||> &r
|||||=============================
|||||Step 325
|||||
|||||? (((r v (q v p)) v (((~ r) v q) v (r v q))) & ((r v (q v p)) v (((~ r) v q) v (r v (~ r)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 326
||||||
||||||? ((r v (q v p)) v (((~ r) v q) v (r v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 327
||||||
||||||? r
||||||
||||||1. (~ q)
||||||2. r
||||||3. (~ p)
||||||
||||||> hyp
|||||=============================
|||||Step 328
|||||
|||||? ((r v (q v p)) v (((~ r) v q) v (r v (~ r))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 329
|||||
|||||? (~ r)
|||||
|||||1. (~ r)
|||||2. (~ q)
|||||3. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 330
||||
||||? (((r v (q v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 331
|||||
|||||? ((r v (q v p)) v (((~ r) v q) v ((~ q) v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 332
|||||
|||||? q
|||||
|||||1. q
|||||2. r
|||||3. (~ p)
|||||4. (~ r)
|||||
|||||> hyp
||||=============================
||||Step 333
||||
||||? ((r v (q v p)) v (((~ r) v q) v ((~ q) v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 334
||||
||||? (~ r)
||||
||||1. q
||||2. (~ q)
||||3. (~ p)
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 335
|||
|||? ((((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 336
||||
||||? (((r v (q v (~ q))) v (((~ r) v q) v (r v q))) & ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 337
|||||
|||||? ((r v (q v (~ q))) v (((~ r) v q) v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 338
|||||
|||||? q
|||||
|||||1. (~ r)
|||||2. r
|||||3. q
|||||
|||||> hyp
||||=============================
||||Step 339
||||
||||? ((r v (q v (~ q))) v (((~ r) v q) v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 340
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. (~ q)
||||3. q
||||
||||> hyp
|||=============================
|||Step 341
|||
|||? (((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 342
||||
||||? ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 343
||||
||||? q
||||
||||1. q
||||2. r
||||3. (~ r)
||||
||||> hyp
|||=============================
|||Step 344
|||
|||? ((r v (q v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 345
|||
|||? (~ r)
|||
|||1. q
|||2. (~ q)
|||3. (~ r)
|||
|||> hyp
||=============================
||Step 346
||
||? ((((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))))))
||
||
||> &r
|||=============================
|||Step 347
|||
|||? (((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r)))))))
|||
|||
|||> &r
||||=============================
||||Step 348
||||
||||? ((((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r))))))
||||
||||
||||> &r
|||||=============================
|||||Step 349
|||||
|||||? (((r v ((~ p) v p)) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r)))))
|||||
|||||
|||||> &r
||||||=============================
||||||Step 350
||||||
||||||? ((r v ((~ p) v p)) v (((~ q) v r) v (r v q)))
||||||
||||||
||||||> hypdisj
||||||=============================
||||||Step 351
||||||
||||||? q
||||||
||||||1. (~ r)
||||||2. q
||||||3. (~ p)
||||||4. p
||||||
||||||> hyp
|||||=============================
|||||Step 352
|||||
|||||? ((r v ((~ p) v p)) v (((~ q) v r) v (r v (~ r))))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 353
|||||
|||||? (~ r)
|||||
|||||1. (~ r)
|||||2. q
|||||3. (~ p)
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 354
||||
||||? (((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 355
|||||
|||||? ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 356
|||||
|||||? q
|||||
|||||1. q
|||||2. (~ r)
|||||3. (~ p)
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 357
||||
||||? ((r v ((~ p) v p)) v (((~ q) v r) v ((~ q) v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 358
||||
||||? (~ r)
||||
||||1. q
||||2. (~ r)
||||3. (~ p)
||||4. p
||||
||||> hyp
|||=============================
|||Step 359
|||
|||? ((((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 360
||||
||||? (((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 361
|||||
|||||? ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 362
|||||
|||||? q
|||||
|||||1. (~ r)
|||||2. q
|||||3. p
|||||
|||||> hyp
||||=============================
||||Step 363
||||
||||? ((r v ((~ p) v (~ q))) v (((~ q) v r) v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 364
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. q
||||3. p
||||
||||> hyp
|||=============================
|||Step 365
|||
|||? (((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 366
||||
||||? ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 367
||||
||||? q
||||
||||1. q
||||2. (~ r)
||||3. p
||||
||||> hyp
|||=============================
|||Step 368
|||
|||? ((r v ((~ p) v (~ q))) v (((~ q) v r) v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 369
|||
|||? (~ r)
|||
|||1. q
|||2. (~ r)
|||3. p
|||
|||> hyp
||=============================
||Step 370
||
||? (((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))))
||
||
||> &r
|||=============================
|||Step 371
|||
|||? ((((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 372
||||
||||? (((r v ((~ p) v p)) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 373
|||||
|||||? ((r v ((~ p) v p)) v (((~ r) v q) v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 374
|||||
|||||? r
|||||
|||||1. (~ q)
|||||2. r
|||||3. (~ p)
|||||4. p
|||||
|||||> hyp
||||=============================
||||Step 375
||||
||||? ((r v ((~ p) v p)) v (((~ r) v q) v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 376
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. (~ q)
||||3. (~ p)
||||4. p
||||
||||> hyp
|||=============================
|||Step 377
|||
|||? (((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 378
||||
||||? ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 379
||||
||||? q
||||
||||1. q
||||2. r
||||3. (~ p)
||||4. p
||||5. (~ r)
||||
||||> hyp
|||=============================
|||Step 380
|||
|||? ((r v ((~ p) v p)) v (((~ r) v q) v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 381
|||
|||? (~ r)
|||
|||1. q
|||2. (~ q)
|||3. (~ p)
|||4. p
|||5. (~ r)
|||
|||> hyp
||=============================
||Step 382
||
||? ((((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 383
|||
|||? (((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 384
||||
||||? ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 385
||||
||||? q
||||
||||1. (~ r)
||||2. r
||||3. q
||||4. p
||||
||||> hyp
|||=============================
|||Step 386
|||
|||? ((r v ((~ p) v (~ q))) v (((~ r) v q) v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 387
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. (~ q)
|||3. q
|||4. p
|||
|||> hyp
||=============================
||Step 388
||
||? (((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 389
|||
|||? ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 390
|||
|||? q
|||
|||1. q
|||2. r
|||3. p
|||4. (~ r)
|||
|||> hyp
||=============================
||Step 391
||
||? ((r v ((~ p) v (~ q))) v (((~ r) v q) v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 392
||
||? (~ r)
||
||1. q
||2. (~ q)
||3. p
||4. (~ r)
||
||> hyp
|=============================
|Step 393
|
|? ((((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q))))) & ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q)))))) & ((((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r)))))))))
|
|
|> &r
||=============================
||Step 394
||
||? (((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q))))) & ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q))))))
||
||
||> &r
|||=============================
|||Step 395
|||
|||? ((((~ p) v p) v (r v (q v p))) & (((~ p) v p) v (r v (q v (~ q)))))
|||
|||
|||> &r
||||=============================
||||Step 396
||||
||||? (((~ p) v p) v (r v (q v p)))
||||
||||
||||> hypdisj
||||=============================
||||Step 397
||||
||||? p
||||
||||1. (~ q)
||||2. (~ r)
||||3. p
||||
||||> hyp
|||=============================
|||Step 398
|||
|||? (((~ p) v p) v (r v (q v (~ q))))
|||
|||
|||> hypdisj
|||=============================
|||Step 399
|||
|||? (~ q)
|||
|||1. (~ q)
|||2. (~ r)
|||3. (~ p)
|||4. p
|||
|||> hyp
||=============================
||Step 400
||
||? ((((~ p) v p) v (r v ((~ p) v p))) & (((~ p) v p) v (r v ((~ p) v (~ q)))))
||
||
||> &r
|||=============================
|||Step 401
|||
|||? (((~ p) v p) v (r v ((~ p) v p)))
|||
|||
|||> hypdisj
|||=============================
|||Step 402
|||
|||? p
|||
|||1. p
|||2. (~ r)
|||
|||> hyp
||=============================
||Step 403
||
||? (((~ p) v p) v (r v ((~ p) v (~ q))))
||
||
||> hypdisj
||=============================
||Step 404
||
||? (~ p)
||
||1. q
||2. (~ r)
||3. (~ p)
||
||> hyp
|=============================
|Step 405
|
|? ((((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))) & (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r))))))))
|
|
|> &r
||=============================
||Step 406
||
||? (((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r)))))))
||
||
||> &r
|||=============================
|||Step 407
|||
|||? ((((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r))))) & (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 408
||||
||||? (((r v (q v p)) v ((~ p) v (r v q))) & ((r v (q v p)) v ((~ p) v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 409
|||||
|||||? ((r v (q v p)) v ((~ p) v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 410
|||||
|||||? (~ p)
|||||
|||||1. (~ q)
|||||2. (~ r)
|||||3. (~ p)
|||||
|||||> hyp
||||=============================
||||Step 411
||||
||||? ((r v (q v p)) v ((~ p) v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 412
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. p
||||3. (~ p)
||||4. (~ q)
||||
||||> hyp
|||=============================
|||Step 413
|||
|||? (((r v (q v p)) v ((~ p) v ((~ q) v q))) & ((r v (q v p)) v ((~ p) v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 414
||||
||||? ((r v (q v p)) v ((~ p) v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 415
||||
||||? q
||||
||||1. q
||||2. p
||||3. (~ p)
||||4. (~ r)
||||
||||> hyp
|||=============================
|||Step 416
|||
|||? ((r v (q v p)) v ((~ p) v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 417
|||
|||? (~ r)
|||
|||1. q
|||2. p
|||3. (~ p)
|||4. (~ q)
|||5. (~ r)
|||
|||> hyp
||=============================
||Step 418
||
||? ((((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 419
|||
|||? (((r v (q v (~ q))) v ((~ p) v (r v q))) & ((r v (q v (~ q))) v ((~ p) v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 420
||||
||||? ((r v (q v (~ q))) v ((~ p) v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 421
||||
||||? q
||||
||||1. (~ r)
||||2. p
||||3. q
||||
||||> hyp
|||=============================
|||Step 422
|||
|||? ((r v (q v (~ q))) v ((~ p) v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 423
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. p
|||3. q
|||4. (~ q)
|||
|||> hyp
||=============================
||Step 424
||
||? (((r v (q v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 425
|||
|||? ((r v (q v (~ q))) v ((~ p) v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 426
|||
|||? q
|||
|||1. q
|||2. p
|||3. (~ r)
|||
|||> hyp
||=============================
||Step 427
||
||? ((r v (q v (~ q))) v ((~ p) v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 428
||
||? (~ r)
||
||1. q
||2. p
||3. (~ q)
||4. (~ r)
||
||> hyp
|=============================
|Step 429
|
|? (((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))) & ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r)))))))
|
|
|> &r
||=============================
||Step 430
||
||? ((((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 431
|||
|||? (((r v ((~ p) v p)) v ((~ p) v (r v q))) & ((r v ((~ p) v p)) v ((~ p) v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 432
||||
||||? ((r v ((~ p) v p)) v ((~ p) v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 433
||||
||||? (~ p)
||||
||||1. (~ q)
||||2. (~ r)
||||3. (~ p)
||||
||||> hyp
|||=============================
|||Step 434
|||
|||? ((r v ((~ p) v p)) v ((~ p) v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 435
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. p
|||3. (~ p)
|||
|||> hyp
||=============================
||Step 436
||
||? (((r v ((~ p) v p)) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 437
|||
|||? ((r v ((~ p) v p)) v ((~ p) v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 438
|||
|||? q
|||
|||1. q
|||2. p
|||3. (~ p)
|||4. (~ r)
|||
|||> hyp
||=============================
||Step 439
||
||? ((r v ((~ p) v p)) v ((~ p) v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 440
||
||? (~ r)
||
||1. q
||2. p
||3. (~ p)
||4. (~ r)
||
||> hyp
|=============================
|Step 441
|
|? ((((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))) & (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r))))))
|
|
|> &r
||=============================
||Step 442
||
||? (((r v ((~ p) v (~ q))) v ((~ p) v (r v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r)))))
||
||
||> &r
|||=============================
|||Step 443
|||
|||? ((r v ((~ p) v (~ q))) v ((~ p) v (r v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 444
|||
|||? q
|||
|||1. (~ r)
|||2. p
|||3. q
|||
|||> hyp
||=============================
||Step 445
||
||? ((r v ((~ p) v (~ q))) v ((~ p) v (r v (~ r))))
||
||
||> hypdisj
||=============================
||Step 446
||
||? (~ r)
||
||1. (~ r)
||2. p
||3. q
||
||> hyp
|=============================
|Step 447
|
|? (((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q))) & ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r)))))
|
|
|> &r
||=============================
||Step 448
||
||? ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v q)))
||
||
||> hypdisj
||=============================
||Step 449
||
||? q
||
||1. q
||2. p
||3. (~ r)
||
||> hyp
|=============================
|Step 450
|
|? ((r v ((~ p) v (~ q))) v ((~ p) v ((~ q) v (~ r))))
|
|
|> hypdisj
|=============================
|Step 451
|
|? (~ r)
|
|1. q
|2. p
|3. (~ r)
|
|> hyp
=============================
Step 452

? (((((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v p)) & (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r)))))))) & ((((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v p)) & (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r)))))))))


> &r
|=============================
|Step 453
|
|? ((((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v p)) & (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r))))))))
|
|
|> &r
||=============================
||Step 454
||
||? (((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r))))))))
||
||
||> &r
|||=============================
|||Step 455
|||
|||? ((((~ r) v ((~ p) v q)) v (p v ((~ q) v r))) & (((~ r) v ((~ p) v q)) v (p v ((~ r) v q))))
|||
|||
|||> &r
||||=============================
||||Step 456
||||
||||? (((~ r) v ((~ p) v q)) v (p v ((~ q) v r)))
||||
||||
||||> hypdisj
||||=============================
||||Step 457
||||
||||? r
||||
||||1. q
||||2. (~ p)
||||3. (~ q)
||||4. p
||||5. r
||||
||||> hyp
|||=============================
|||Step 458
|||
|||? (((~ r) v ((~ p) v q)) v (p v ((~ r) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 459
|||
|||? p
|||
|||1. (~ q)
|||2. r
|||3. p
|||
|||> hyp
||=============================
||Step 460
||
||? ((((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))))
||
||
||> &r
|||=============================
|||Step 461
|||
|||? (((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r))))))
|||
|||
|||> &r
||||=============================
||||Step 462
||||
||||? ((((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r)))))
||||
||||
||||> &r
|||||=============================
|||||Step 463
|||||
|||||? (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v q)))
|||||
|||||
|||||> hypdisj
|||||=============================
|||||Step 464
|||||
|||||? q
|||||
|||||1. (~ r)
|||||2. q
|||||3. p
|||||4. r
|||||
|||||> hyp
||||=============================
||||Step 465
||||
||||? (((~ r) v ((~ p) v q)) v (((~ q) v r) v (r v (~ r))))
||||
||||
||||> hypdisj
||||=============================
||||Step 466
||||
||||? (~ r)
||||
||||1. (~ r)
||||2. q
||||3. (~ q)
||||4. p
||||
||||> hyp
|||=============================
|||Step 467
|||
|||? ((((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 468
||||
||||? (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 469
||||
||||? q
||||
||||1. q
||||2. (~ r)
||||3. p
||||4. r
||||
||||> hyp
|||=============================
|||Step 470
|||
|||? (((~ r) v ((~ p) v q)) v (((~ q) v r) v ((~ q) v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 471
|||
|||? (~ r)
|||
|||1. q
|||2. (~ r)
|||3. (~ q)
|||4. p
|||
|||> hyp
||=============================
||Step 472
||
||? (((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 473
|||
|||? ((((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 474
||||
||||? (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 475
||||
||||? r
||||
||||1. (~ q)
||||2. r
||||3. p
||||
||||> hyp
|||=============================
|||Step 476
|||
|||? (((~ r) v ((~ p) v q)) v (((~ r) v q) v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 477
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. (~ q)
|||3. p
|||
|||> hyp
||=============================
||Step 478
||
||? ((((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 479
|||
|||? (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 480
|||
|||? q
|||
|||1. q
|||2. r
|||3. p
|||
|||> hyp
||=============================
||Step 481
||
||? (((~ r) v ((~ p) v q)) v (((~ r) v q) v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 482
||
||? (~ q)
||
||1. r
||2. (~ q)
||3. p
||
||> hyp
|=============================
|Step 483
|
|? ((((~ r) v ((~ p) v q)) v ((~ p) v p)) & (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r)))))))
|
|
|> &r
||=============================
||Step 484
||
||? (((~ r) v ((~ p) v q)) v ((~ p) v p))
||
||
||> hypdisj
||=============================
||Step 485
||
||? p
||
||1. p
||2. (~ q)
||3. r
||
||> hyp
|=============================
|Step 486
|
|? (((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r))))))
|
|
|> &r
||=============================
||Step 487
||
||? ((((~ r) v ((~ p) v q)) v ((~ p) v (r v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r)))))
||
||
||> &r
|||=============================
|||Step 488
|||
|||? (((~ r) v ((~ p) v q)) v ((~ p) v (r v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 489
|||
|||? r
|||
|||1. (~ q)
|||2. p
|||3. r
|||
|||> hyp
||=============================
||Step 490
||
||? (((~ r) v ((~ p) v q)) v ((~ p) v (r v (~ r))))
||
||
||> hypdisj
||=============================
||Step 491
||
||? (~ r)
||
||1. (~ r)
||2. p
||3. (~ q)
||
||> hyp
|=============================
|Step 492
|
|? ((((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r)))))
|
|
|> &r
||=============================
||Step 493
||
||? (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v q)))
||
||
||> hypdisj
||=============================
||Step 494
||
||? q
||
||1. q
||2. p
||3. r
||
||> hyp
|=============================
|Step 495
|
|? (((~ r) v ((~ p) v q)) v ((~ p) v ((~ q) v (~ r))))
|
|
|> hypdisj
|=============================
|Step 496
|
|? (~ q)
|
|1. r
|2. p
|3. (~ q)
|
|> hyp
=============================
Step 497

? ((((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v p)) & (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r))))))))


> &r
|=============================
|Step 498
|
|? (((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))) & ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r))))))))
|
|
|> &r
||=============================
||Step 499
||
||? ((((~ r) v ((~ q) v p)) v (p v ((~ q) v r))) & (((~ r) v ((~ q) v p)) v (p v ((~ r) v q))))
||
||
||> &r
|||=============================
|||Step 500
|||
|||? (((~ r) v ((~ q) v p)) v (p v ((~ q) v r)))
|||
|||
|||> hypdisj
|||=============================
|||Step 501
|||
|||? r
|||
|||1. q
|||2. (~ p)
|||3. r
|||
|||> hyp
||=============================
||Step 502
||
||? (((~ r) v ((~ q) v p)) v (p v ((~ r) v q)))
||
||
||> hypdisj
||=============================
||Step 503
||
||? q
||
||1. r
||2. (~ p)
||3. q
||
||> hyp
|=============================
|Step 504
|
|? ((((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))) & (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))))
|
|
|> &r
||=============================
||Step 505
||
||? (((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r))))))
||
||
||> &r
|||=============================
|||Step 506
|||
|||? ((((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r)))))
|||
|||
|||> &r
||||=============================
||||Step 507
||||
||||? (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v q)))
||||
||||
||||> hypdisj
||||=============================
||||Step 508
||||
||||? q
||||
||||1. (~ r)
||||2. q
||||3. (~ p)
||||4. r
||||
||||> hyp
|||=============================
|||Step 509
|||
|||? (((~ r) v ((~ q) v p)) v (((~ q) v r) v (r v (~ r))))
|||
|||
|||> hypdisj
|||=============================
|||Step 510
|||
|||? (~ r)
|||
|||1. (~ r)
|||2. q
|||3. (~ p)
|||
|||> hyp
||=============================
||Step 511
||
||? ((((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r)))))
||
||
||> &r
|||=============================
|||Step 512
|||
|||? (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 513
|||
|||? q
|||
|||1. q
|||2. (~ r)
|||3. (~ p)
|||4. r
|||
|||> hyp
||=============================
||Step 514
||
||? (((~ r) v ((~ q) v p)) v (((~ q) v r) v ((~ q) v (~ r))))
||
||
||> hypdisj
||=============================
||Step 515
||
||? (~ r)
||
||1. q
||2. (~ r)
||3. (~ p)
||
||> hyp
|=============================
|Step 516
|
|? (((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r))))))
|
|
|> &r
||=============================
||Step 517
||
||? ((((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r)))))
||
||
||> &r
|||=============================
|||Step 518
|||
|||? (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v q)))
|||
|||
|||> hypdisj
|||=============================
|||Step 519
|||
|||? q
|||
|||1. (~ r)
|||2. r
|||3. (~ p)
|||4. q
|||
|||> hyp
||=============================
||Step 520
||
||? (((~ r) v ((~ q) v p)) v (((~ r) v q) v (r v (~ r))))
||
||
||> hypdisj
||=============================
||Step 521
||
||? (~ r)
||
||1. (~ r)
||2. (~ q)
||3. (~ p)
||4. q
||
||> hyp
|=============================
|Step 522
|
|? ((((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r)))))
|
|
|> &r
||=============================
||Step 523
||
||? (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v q)))
||
||
||> hypdisj
||=============================
||Step 524
||
||? q
||
||1. q
||2. r
||3. (~ p)
||
||> hyp
|=============================
|Step 525
|
|? (((~ r) v ((~ q) v p)) v (((~ r) v q) v ((~ q) v (~ r))))
|
|
|> hypdisj
|=============================
|Step 526
|
|? (~ q)
|
|1. r
|2. (~ q)
|3. (~ p)
|
|> hyp
=============================
Step 527

? ((((~ r) v ((~ q) v p)) v ((~ p) v p)) & (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r)))))))


> &r
|=============================
|Step 528
|
|? (((~ r) v ((~ q) v p)) v ((~ p) v p))
|
|
|> hypdisj
|=============================
|Step 529
|
|? p
|
|1. p
|2. q
|3. r
|
|> hyp
=============================
Step 530

? (((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))) & ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r))))))


> &r
|=============================
|Step 531
|
|? ((((~ r) v ((~ q) v p)) v ((~ p) v (r v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r)))))
|
|
|> &r
||=============================
||Step 532
||
||? (((~ r) v ((~ q) v p)) v ((~ p) v (r v q)))
||
||
||> hypdisj
||=============================
||Step 533
||
||? q
||
||1. (~ r)
||2. p
||3. (~ p)
||4. q
||5. r
||
||> hyp
|=============================
|Step 534
|
|? (((~ r) v ((~ q) v p)) v ((~ p) v (r v (~ r))))
|
|
|> hypdisj
|=============================
|Step 535
|
|? (~ r)
|
|1. (~ r)
|2. p
|3. (~ p)
|4. q
|
|> hyp
=============================
Step 536

? ((((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q))) & (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r)))))


> &r
|=============================
|Step 537
|
|? (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v q)))
|
|
|> hypdisj
|=============================
|Step 538
|
|? q
|
|1. q
|2. p
|3. (~ p)
|4. r
|
|> hyp
=============================
Step 539

? (((~ r) v ((~ q) v p)) v ((~ p) v ((~ q) v (~ r))))


> hypdisj
=============================
Step 540

? (~ p)

1. r
2. q
3. (~ p)

> hyp
